\begin{nusmvCommand} {check\_ltlspec\_bmc} {\label{checkLtlspecBmcCoomand} 
Checks the given LTL specification, or all LTL specifications if no
formula is given.  Checking parameters are the maximum length and the
loopback value}

\cmdLine{check\_ltlspec\_bmc [-h | -n idx | -p "formula [IN context]"]
[-k max\_length] [-l loopback] [-o filename]}

This command generates one or more problems, and calls SAT solver for
each one. Each problem is related to a specific problem bound, which
increases from zero ($0$) to the given maximum problem length. Here
\code{max\_length} is the bound of the problem that system is going to
generate and solve.  In this context the maximum problem bound is
represented by the \commandopt{k} command parameter, or by its default
value stored in the environment variable \envvar{bmc\_length}.  The
single generated problem also depends on the \code{loopback} parameter
you can explicitly specify by the \commandopt{l} option, or by its
default value stored in the environment variable
\envvar{bmc\_loopback}.

The property to be checked may be specified using the \commandopt{n
idx} or the \commandopt{p "formula"} options.  If you need to generate
a DIMACS dump file of all generated problems, you must use the option
\command{-o "filename"}.

\begin{cmdOpt}

\opt{-n \parameter{\natnum{\it index}}}{\natnum{\it index} is the
numeric index of a valid LTL specification formula actually located in
the properties database.}
       
\opt{-p \parameter{"\anyexpr [IN context]"}}{Checks the \anyexpr specified on
the command-line. \code{context} is the module instance name which
the variables in \anyexpr must be evaluated in.}
            
\opt{-k \parameter{\natnum{\it max\_length}}}{\natnum{\it max\_length} is the maximum problem
bound to be checked. Only natural numbers are valid values for this
option. If no value is given the environment variable \envvar{\it
bmc\_length} is considered instead.}

\opt{-l \parameter{\set{\it loopback}{\range{0}{max\_length-1},
       \range{-1}{bmc\_length}, X, *}}}{The {\it loopback} value may be: }
       \tabItem{a natural number in (0, {\it max\_length-1}). A positive sign (`+')
       can be also used as prefix of the number. Any invalid
       combination of length and loopback will be skipped during the
       generation/solving process.}
       \tabItem{a negative number in
       (-1, -{\it bmc\_length}). In this case {\it loopback} is
       considered a value relative to {\it max\_length}.  Any invalid
       combination of length and loopback will be skipped during the
       generation/solving process.}
       \tabItem{the symbol
       `\varvalue{X}', which means ``no loopback".}
       \tabItem{the
       symbol `\varvalue{*}', which means ``all possible loopbacks from
       zero to {\it length-1}" .}

\opt{-o \parameter{\filename{\it filename}}}{\filename{\it filename} is the name of the dumped
dimacs file.  It may contain special symbols which will be
macro-expanded to form the real file name. Possible symbols are: }
       \tabItem{@F: model name with path part. }
       \tabItem{@f: model name without path part.} 
       \tabItem{@k: current problem bound.} 
       \tabItem{@l: current loopback value.} 
       \tabItem{@n: index of the currently processed formula in the property 
       database.} 
       \tabItem{@@: the `@' character.}

\end{cmdOpt}
\end{nusmvCommand}
